﻿
#include <iostream>
#include <sstream>
#include <cstdlib>

#include "../divine/generator/simulink.h"
#include "../divine/generator/custom-api.h"

// Automatically generated from XML system
struct VoterCore3:Block {
  Constant< int > unique_constant_1i3sa4x6y4u;
  Constant< int > constant_Constant_1;
  Constant< int > constant1_Constant_1;
  Constant< int > constant2_Constant_1;
  Constant< int > constant3_Constant_1;
  Constant< int > constant4_Constant_1;
  Constant< int > constant5_Constant_1;
  Constant< int > constant8_Constant_1;
  RelationalOperator< int > greaterEq_Greater_1;
  RelationalOperator< int > greaterEq1_Greater_1;
  RelationalOperator< int > greaterEq2_Greater_1;
  RelationalOperator< int > greaterThan_Greater_1;
  RelationalOperator< int > greaterThan1_Greater_1;
  RelationalOperator< int > greaterThan2_Greater_1;
  MinMax< int > min_Minmax_1;
  MinMax< int > min1_Minmax_1;
  MinMax< int > min2_Minmax_1;
  Logic< bool > not_Not_1;
  Logic< bool > not1_Not_1;
  Logic< bool > not2_Not_1;
  Logic< bool > or_Or_1;
  Logic< bool > or1_Or_1;
  Logic< bool > or2_Or_1;
  UnitDelay< int > simpleDelay_SimpleDelay_1;
  UnitDelay< int > simpleDelay1_SimpleDelay_1;
  UnitDelay< int > simpleDelay2_SimpleDelay_1;
  Sum< int > sum_Sum_1;
  Sum< int > sum1_Sum_1;
  Sum< int > sum2_Sum_1;
  Switch< int > switch_Switch_1;
  Switch< int > switch1_Switch_1;
  Switch< int > switch2_Switch_1;
  DataTypeConversion< bool, int > typecast_tCast_1;
  DataTypeConversion< bool, int > typecast1_tCast_1;
  DataTypeConversion< bool, int > typecast2_tCast_1;
  Inport< int > signal_delta23;
  Inport< int > signal_delta13;
  Inport< int > signal_delta12;
  Inport< bool > signal_valid1;
  Inport< bool > signal_valid2;
  Inport< bool > signal_valid3;
  Outport< bool > signal_mismatch1;
  Outport< bool > signal_mismatch2;
  Outport< bool > signal_mismatch3;
  Outport< bool > permanent_mismatch1;
  Outport< bool > permanent_mismatch2;
  Outport< bool > permanent_mismatch3;

  VoterCore3(): constant_Constant_1( 1 ), constant1_Constant_1( 1 ), constant2_Constant_1( 1 ), constant3_Constant_1( 3 ), constant4_Constant_1( 0 ), constant5_Constant_1( 0 ), constant8_Constant_1( 0 ), not_Not_1( Logic< bool >:: NOT ), not1_Not_1( Logic< bool >:: NOT ), not2_Not_1( Logic< bool >:: NOT ), or_Or_1( Logic< bool >:: OR ), or1_Or_1( Logic< bool >:: OR ), or2_Or_1( Logic< bool >:: OR ), min_Minmax_1( MinMax< int > ::min), min1_Minmax_1( MinMax< int > ::min), min2_Minmax_1( MinMax< int > ::min), greaterEq_Greater_1( RelationalOperator < int > ::GE ), greaterEq1_Greater_1( RelationalOperator < int > ::GE ), greaterEq2_Greater_1( RelationalOperator < int > ::GE ), greaterThan_Greater_1( RelationalOperator < int > ::GT ), greaterThan1_Greater_1( RelationalOperator < int > ::GT ), greaterThan2_Greater_1( RelationalOperator < int > ::GT ),  unique_constant_1i3sa4x6y4u( 0 ) {

    signal_delta23 = Inport< int >( 0, 3, "signal_delta23" );
    signal_delta13 = Inport< int >( 0, 3, "signal_delta13" );
    signal_delta12 = Inport< int >( 0, 3, "signal_delta12" );
    signal_valid1 = Inport< bool >( 0, 1, "signal_valid1" );
    signal_valid2 = Inport< bool >( 0, 1, "signal_valid2" );
    signal_valid3 = Inport< bool >( 0, 1, "signal_valid3" );

    signal_mismatch1 = Outport< bool >( "signal_mismatch1" );
    signal_mismatch2 = Outport< bool >( "signal_mismatch2" );
    signal_mismatch3 = Outport< bool >( "signal_mismatch3" );
    permanent_mismatch1 = Outport< bool >( "permanent_mismatch1" );
    permanent_mismatch2 = Outport< bool >( "permanent_mismatch2" );
    permanent_mismatch3 = Outport< bool >( "permanent_mismatch3" );

    simpleDelay_SimpleDelay_1 = UnitDelay< int >( "simpleDelay_SimpleDelay_1" );
    simpleDelay1_SimpleDelay_1 = UnitDelay< int >( "simpleDelay1_SimpleDelay_1" );
    simpleDelay2_SimpleDelay_1 = UnitDelay< int >( "simpleDelay2_SimpleDelay_1" );
    
    connect( constant1_Constant_1, greaterThan1_Greater_1, 1 );		// constant1( 1 ), greaterThan1( b )
    connect( constant_Constant_1, greaterThan_Greater_1, 1 );		// constant( 1 ), greaterThan( b )
    connect( constant2_Constant_1, greaterThan2_Greater_1, 1 );		// constant2( 1 ), greaterThan2( b )
    connect( greaterThan_Greater_1, or_Or_1, 0 );		// greaterThan( a>b ), or( 1 )
    connect( greaterThan1_Greater_1, or1_Or_1, 0 );		// greaterThan1( a>b ), or1( 1 )
    connect( greaterThan2_Greater_1, or2_Or_1, 0 );		// greaterThan2( a>b ), or2( 1 )
    connect( signal_valid1, not_Not_1, 0 );		// signal_valid1( 1 ), not( 1 )
    connect( signal_valid2, not1_Not_1, 0 );		// signal_valid2( 1 ), not1( 1 )
    connect( signal_valid3, not2_Not_1, 0 );		// signal_valid3( 1 ), not2( 1 )
    connect( or_Or_1, signal_mismatch1, 0 );		// or( 1000 ), signal_mismatch1( 1 )
    connect( or_Or_1, typecast_tCast_1, 0 );		// or( 1000 ), typecast( In1 )
    connect( or1_Or_1, signal_mismatch2, 0 );		// or1( 1000 ), signal_mismatch2( 1 )
    connect( or1_Or_1, typecast1_tCast_1, 0 );		// or1( 1000 ), typecast1( In1 )
    connect( or2_Or_1, signal_mismatch3, 0 );		// or2( 1000 ), signal_mismatch3( 1 )
    connect( or2_Or_1, typecast2_tCast_1, 0 );		// or2( 1000 ), typecast2( In1 )
    connect( not_Not_1, or_Or_1, 1 );		// not( 2 ), or( 2 )
    connect( not1_Not_1, or1_Or_1, 1 );		// not1( 2 ), or1( 2 )
    connect( not2_Not_1, or2_Or_1, 1 );		// not2( 2 ), or2( 2 )
    connect( sum_Sum_1, simpleDelay_SimpleDelay_1, 0 );		// sum( 1000 ), simpleDelay( 1 )
    connect( sum_Sum_1, greaterEq_Greater_1, 0 );		// sum( 1000 ), greaterEq( a )
    connect( simpleDelay_SimpleDelay_1, switch_Switch_1, 0 );		// simpleDelay( 2 ), switch( 1 )
    connect( typecast_tCast_1, sum_Sum_1, 0 );		// typecast( Out1 ), sum( 1 )
    connect( typecast_tCast_1, switch_Switch_1, 1 );		// typecast( Out1 ), switch( 3 )
    connect( constant8_Constant_1, switch_Switch_1, 2 );		// constant8( 1 ), switch( 2 )
    connect( sum1_Sum_1, simpleDelay1_SimpleDelay_1, 0 );		// sum1( 1000 ), simpleDelay1( 1 )
    connect( sum1_Sum_1, greaterEq1_Greater_1, 0 );		// sum1( 1000 ), greaterEq1( a )
    connect( simpleDelay1_SimpleDelay_1, switch1_Switch_1, 0 );		// simpleDelay1( 2 ), switch1( 1 )
    connect( typecast1_tCast_1, sum1_Sum_1, 0 );		// typecast1( Out1 ), sum1( 1 )
    connect( typecast1_tCast_1, switch1_Switch_1, 1 );		// typecast1( Out1 ), switch1( 3 )
    connect( constant4_Constant_1, switch1_Switch_1, 2 );		// constant4( 1 ), switch1( 2 )
    connect( sum2_Sum_1, simpleDelay2_SimpleDelay_1, 0 );		// sum2( 1000 ), simpleDelay2( 1 )
    connect( sum2_Sum_1, greaterEq2_Greater_1, 0 );		// sum2( 1000 ), greaterEq2( a )
    connect( simpleDelay2_SimpleDelay_1, switch2_Switch_1, 0 );		// simpleDelay2( 2 ), switch2( 1 )
    connect( typecast2_tCast_1, sum2_Sum_1, 0 );		// typecast2( Out1 ), sum2( 1 )
    connect( typecast2_tCast_1, switch2_Switch_1, 1 );		// typecast2( Out1 ), switch2( 3 )
    connect( constant5_Constant_1, switch2_Switch_1, 2 );		// constant5( 1 ), switch2( 2 )
    connect( greaterEq_Greater_1, permanent_mismatch1, 0 );		// greaterEq( a>=b ), permanent_mismatch1( 1 )
    connect( greaterEq1_Greater_1, permanent_mismatch2, 0 );		// greaterEq1( a>=b ), permanent_mismatch2( 1 )
    connect( greaterEq2_Greater_1, permanent_mismatch3, 0 );		// greaterEq2( a>=b ), permanent_mismatch3( 1 )
    connect( signal_delta23, greaterThan_Greater_1, 0 );		// signal_delta23( 1 ), greaterThan( a )
    connect( signal_delta13, greaterThan1_Greater_1, 0 );		// signal_delta13( 1 ), greaterThan1( a )
    connect( signal_delta12, greaterThan2_Greater_1, 0 );		// signal_delta12( 1 ), greaterThan2( a )
    connect( constant3_Constant_1, greaterEq_Greater_1, 1 );		// constant3( 1 ), greaterEq( b )
    connect( constant3_Constant_1, greaterEq1_Greater_1, 1 );		// constant3( 1 ), greaterEq1( b )
    connect( constant3_Constant_1, greaterEq2_Greater_1, 1 );		// constant3( 1 ), greaterEq2( b )
    connect( constant3_Constant_1, min_Minmax_1, 1 );		// constant3( 1 ), min( 2 )
    connect( constant3_Constant_1, min1_Minmax_1, 1 );		// constant3( 1 ), min1( 2 )
    connect( constant3_Constant_1, min2_Minmax_1, 1 );		// constant3( 1 ), min2( 2 )
    connect( switch2_Switch_1, min_Minmax_1, 0 );		// switch2( 4 ), min( 1 )
    connect( min_Minmax_1, sum2_Sum_1, 1 );		// min( 100 ), sum2( 2 )
    connect( min2_Minmax_1, sum_Sum_1, 1 );		// min2( 100 ), sum( 2 )
    connect( min1_Minmax_1, sum1_Sum_1, 1 );		// min1( 100 ), sum1( 2 )
    connect( switch1_Switch_1, min1_Minmax_1, 0 );		// switch1( 4 ), min1( 1 )
    connect( switch_Switch_1, min2_Minmax_1, 0 );		// switch( 4 ), min2( 1 )
  }




};


const int default_range = 8;
#ifdef STANDALONE

const int duration = 30;  

//static int vec[duration] = {0,1,1,0,0,0,1,0,0,1,0,0,0,0,0,1,1,1,1,0,0,0,1,0,0,0,0,1,1};

void VoterCore3_model()
{
    srand((unsigned)time(0));
    std::cout << "VoterCore3 started" << std::endl;
    std::ostringstream signals[168];
    VoterCore3 model;
    SymSystem *sys = new SymSystem( model );
    sys->_circuit = &model;

    for (int i = 0; i < duration; i++)
    {
        model.signal_delta23 = rand() % default_range;
        model.signal_delta13 = rand() % default_range;
        model.signal_delta12 = rand() % default_range;
        model.signal_valid1 = rand() % 2;
        model.signal_valid2 = rand() % 2;
        model.signal_valid3 = rand() % 2;
        signals[0] << model.signal_delta23.get() << ' ';
        signals[1] << model.signal_delta13.get() << ' ';
        signals[2] << model.signal_delta12.get() << ' ';
        signals[3] << model.signal_valid1.get() << ' ';
        signals[4] << model.signal_valid2.get() << ' ';
        signals[5] << model.signal_valid3.get() << ' ';
        signals[6] << model.signal_mismatch1.get() << ' ';
        signals[7] << model.signal_mismatch2.get() << ' ';
        signals[8] << model.signal_mismatch3.get() << ' ';
        signals[9] << model.permanent_mismatch1.get() << ' ';
        signals[10] << model.permanent_mismatch2.get() << ' ';
        signals[11] << model.permanent_mismatch3.get() << ' ';
        signals[12] << model.constant_Constant_1.get() << ' ';
        signals[13] << model.constant1_Constant_1.get() << ' ';
        signals[14] << model.constant2_Constant_1.get() << ' ';
        signals[15] << model.constant3_Constant_1.get() << ' ';
        signals[16] << model.constant4_Constant_1.get() << ' ';
        signals[17] << model.constant5_Constant_1.get() << ' ';
        signals[18] << model.constant8_Constant_1.get() << ' ';
        signals[19] << model.greaterEq_Greater_1.get() << ' ';
        signals[20] << model.greaterEq1_Greater_1.get() << ' ';
        signals[21] << model.greaterEq2_Greater_1.get() << ' ';
        signals[22] << model.greaterThan_Greater_1.get() << ' ';
        signals[23] << model.greaterThan1_Greater_1.get() << ' ';
        signals[24] << model.greaterThan2_Greater_1.get() << ' ';
        signals[25] << model.min_Minmax_1.get() << ' ';
        signals[26] << model.min1_Minmax_1.get() << ' ';
        signals[27] << model.min2_Minmax_1.get() << ' ';
        signals[28] << model.not_Not_1.get() << ' ';
        signals[29] << model.not1_Not_1.get() << ' ';
        signals[30] << model.not2_Not_1.get() << ' ';
        signals[31] << model.or_Or_1.get() << ' ';
        signals[32] << model.or1_Or_1.get() << ' ';
        signals[33] << model.or2_Or_1.get() << ' ';
        signals[34] << model.simpleDelay_SimpleDelay_1.get() << ' ';
        signals[35] << model.simpleDelay1_SimpleDelay_1.get() << ' ';
        signals[36] << model.simpleDelay2_SimpleDelay_1.get() << ' ';
        signals[37] << model.sum_Sum_1.get() << ' ';
        signals[38] << model.sum1_Sum_1.get() << ' ';
        signals[39] << model.sum2_Sum_1.get() << ' ';
        signals[40] << model.switch_Switch_1.get() << ' ';
        signals[41] << model.switch1_Switch_1.get() << ' ';
        signals[42] << model.switch2_Switch_1.get() << ' ';
        signals[43] << model.typecast_tCast_1.get() << ' ';
        signals[44] << model.typecast1_tCast_1.get() << ' ';
        signals[45] << model.typecast2_tCast_1.get() << ' ';
    
        sys->tick();
    }
    std::cout << "inputs = ";
    std::cout << "\n    signal_delta23	= " << signals[0].str();
    std::cout << "\n    signal_delta13	= " << signals[1].str();
    std::cout << "\n    signal_delta12	= " << signals[2].str();
    std::cout << "\n    signal_valid1	= " << signals[3].str();
    std::cout << "\n    signal_valid2	= " << signals[4].str();
    std::cout << "\n    signal_valid3	= " << signals[5].str();


    std::cout << "\noutputs = ";
    std::cout << "\n    signal_mismatch1	= " << signals[6].str();
    std::cout << "\n    signal_mismatch2	= " << signals[7].str();
    std::cout << "\n    signal_mismatch3	= " << signals[8].str();
    std::cout << "\n    permanent_mismatch1	= " << signals[9].str();
    std::cout << "\n    permanent_mismatch2	= " << signals[10].str();
    std::cout << "\n    permanent_mismatch3	= " << signals[11].str();

    std::cout << "\ninternals = ";
    std::cout << "\n    constant_Constant_1	= " << signals[12].str();
    std::cout << "\n    constant1_Constant_1	= " << signals[13].str();
    std::cout << "\n    constant2_Constant_1	= " << signals[14].str();
    std::cout << "\n    constant3_Constant_1	= " << signals[15].str();
    std::cout << "\n    constant4_Constant_1	= " << signals[16].str();
    std::cout << "\n    constant5_Constant_1	= " << signals[17].str();
    std::cout << "\n    constant8_Constant_1	= " << signals[18].str();
    std::cout << "\n    greaterEq_Greater_1	= " << signals[19].str();
    std::cout << "\n    greaterEq1_Greater_1	= " << signals[20].str();
    std::cout << "\n    greaterEq2_Greater_1	= " << signals[21].str();
    std::cout << "\n    greaterThan_Greater_1	= " << signals[22].str();
    std::cout << "\n    greaterThan1_Greater_1	= " << signals[23].str();
    std::cout << "\n    greaterThan2_Greater_1	= " << signals[24].str();
    std::cout << "\n    min_Minmax_1	= " << signals[25].str();
    std::cout << "\n    min1_Minmax_1	= " << signals[26].str();
    std::cout << "\n    min2_Minmax_1	= " << signals[27].str();
    std::cout << "\n    not_Not_1	= " << signals[28].str();
    std::cout << "\n    not1_Not_1	= " << signals[29].str();
    std::cout << "\n    not2_Not_1	= " << signals[30].str();
    std::cout << "\n    or_Or_1	= " << signals[31].str();
    std::cout << "\n    or1_Or_1	= " << signals[32].str();
    std::cout << "\n    or2_Or_1	= " << signals[33].str();
    std::cout << "\n    simpleDelay_SimpleDelay_1	= " << signals[34].str();
    std::cout << "\n    simpleDelay1_SimpleDelay_1	= " << signals[35].str();
    std::cout << "\n    simpleDelay2_SimpleDelay_1	= " << signals[36].str();
    std::cout << "\n    sum_Sum_1	= " << signals[37].str();
    std::cout << "\n    sum1_Sum_1	= " << signals[38].str();
    std::cout << "\n    sum2_Sum_1	= " << signals[39].str();
    std::cout << "\n    switch_Switch_1	= " << signals[40].str();
    std::cout << "\n    switch1_Switch_1	= " << signals[41].str();
    std::cout << "\n    switch2_Switch_1	= " << signals[42].str();
    std::cout << "\n    typecast_tCast_1	= " << signals[43].str();
    std::cout << "\n    typecast1_tCast_1	= " << signals[44].str();
    std::cout << "\n    typecast2_tCast_1	= " << signals[45].str();
    std::cout << std::endl;

    }

    int main() {
    VoterCore3_model();
}
#endif

#ifndef STANDALONE
static inline char *make( CustomSetup *setup, char **to, int size = 0 )
{
  int total;
  if ( size )
    total = size;
  else
    total = setup->state_size + setup->slack;
  *to = (char *) pool_allocate_blob( setup->cpool, total, setup->slack + 4 );
  return ((*to) + setup->slack + 4); // FIXME; 4 = BlobHeader size
}

SMTSystem &system( CustomSetup *setup )
{
    return *(SMTSystem *)setup->custom;
}

#include "VoterCore3.inc"

extern "C" void get_system_initial( CustomSetup *setup, char **to )
{
  char *v = make( setup, to, system( setup ).size() + setup->slack + 4 + 8 );
  system( setup ).write( v );
}

extern "C" int get_system_successor( CustomSetup *setup, SMTSystem &sys,
                                     int handle, char **to )
{
  if ( handle == 2 )
    return 0;
  sys.tick();
  if ( !sys.pc_sat( true ) )
    return 0;
  *to = (char *)pool_allocate_blob( setup->cpool, sys.size() + setup->slack + 4, setup->slack + 4 );
  sys.write( *to + setup->slack + 4 );

  return 2;
}

extern "C" char *system_show_node( CustomSetup *setup, char *from, int )
{
    char *in = from + setup->slack + 4;
    system( setup ).read( in );
    std::string s = system( setup ).print();
    char *ret = (char *) malloc( s.length() + 1 );
    std::copy( s.begin(), s.end(), ret );
    ret[ s.length() ] = 0;
    return ret;
}

extern "C" void system_setup( CustomSetup *setup )
{
    VoterCore3 *model = new VoterCore3();
    SMTSystem *sys = new SMTSystem( *model );

    setup->state_size = sys->size();
    sys->_smt->offset = setup->slack + 4;
    setup->custom = sys;
}

extern "C" void cache_successors( CustomSetup *setup, SuccessorCache *cache ) {}
#endif
